%!TEX root = /Users/adriaan/src/kinded-scala/papers/oopsla/tcpoly.tex

\begin{figure*}[float=ht]
  \centering
\begin{verbatim}
  TypeParamClause  ::= `[' TypeParam {`,' TypeParam} `]'
  TypeParam        ::=  id [TypeParamClause] [`>:' Type] [`<:' Type]

  AbstractTpMem    ::=  `type' TypeParam  
\end{verbatim}
  \caption{Syntax for type declarations (type parameters and abstract type members)}
  \label{lst:scala:syntax}
\end{figure*}

\begin{figure*}[float=ht]
  \centering
    \includegraphics[width=0.8\textwidth]{hierarchy}
  \caption{Diagram of levels}
  \label{fig:levels}
\end{figure*} 


\section{Of Types and Kinds \label{sec:informalformal}}  % TODO: read Of Mice and Men ;-)
Even though proper types and type constructors are placed on equal footing as far as parametric polymorphism is concerned, one must be careful not to mix them up. Clearly, a type parameter that stands for a proper type, must not be applied to type arguments, whereas a type constructor parameter cannot classify a value until it has been turned into a proper type by supplying the right type arguments.

 In this section we give an informal overview of how programmers may introduce higher-kinded type parameters and abstract type members, and sketch the rules that govern their use. We describe the surface syntax that was introduced with the release of Scala 2.5, and the underlying conceptual model of kinds.  
 

\subsection{Surface syntax for types}
Figure \ref{lst:scala:syntax} shows a simplified fragment of the syntax of type parameters and abstract type members, which we collectively call ``type declarations''. The full syntax, which additionally includes variance annotations, is described in the Scala language specification \cite{odersky:scala-reference}. % full syntax: `_' for higher-order type params, variance annotations, view bounds
Syntactically, our extension introduces an optional \verb|TypeParamClause| as part of a type declaration. The scope of the higher-order type parameters that may thus be introduced, extends over the outer type declaration to which they belong. 

For example, \type{Container[X]} is a valid \verb|TypeParam|, which introduces a type constructor parameter that expects one type argument. To illustrate the scoping of higher-order type parameters, \type{Container[X] <: Iterable[X]} declares a type parameter that, when applied to a type argument \type{Y} -- written as \type{Container[Y]} -- must be a subtype of \type{Iterable[Y]}. 

As a more complicated example, \type{C[X <: Ordered[X]] <: Iterable[X]} introduces a type constructor parameter \type{C}, with an F-bounded higher-order type parameter \type{X}, which occurs in its own bound as well as in the bound of the type parameter that it parameterises.  Thus, \type{C} abstracts over a type constructor so that, for any \type{Y} that is a subtype of \type{Ordered[Y]}, \type{C[Y]} is a subtype of \type{Iterable[Y]} 

 

\subsection{Kinds}
% cannot be expressed directly, inferred by compiler
% simple model: distinguish proper types from type constructors, see diagram
% refine: include bounds, F-bounds: dependent function kind
Conceptually, kinds are used to distinguish a type parameter that stands for a proper type, such as \type{List[Int]}, from a type parameter that abstracts over a type constructor, such as \type{List}. An initial, simplistic kind system is illustrated in the diagram in Fig. \ref{fig:levels}, and it is refined in the remainder of this section. The figure shows the three levels of classification, where entities in lower levels are classified by entities in the layer immediately above them.  

Kinds populate the top layer. The kind \kind{*} classifies types that classify values, and the \kind{->} kind constructor is used to construct kinds that classify type constructors. Note that kinds are inferred by the compiler. They cannot appear in Scala's surface syntax. 



Nonetheless, Fig. \ref{lst:scala:syntax:kinds} introduces syntax for the kinds that classify the types that can be declared as described in the previous section. The first kind, \kind{*(T, U)}, classifies proper types (such as type declarations without higher-order type parameters), and tracks their lower (\type{T}) and upper bounds (\type{U}). It should be clear that this kind is easily inferred, as type declarations either explicitly specify bounds or receive the minimal lower bound, \type{Nothing}, and the maximal upper bound, \type{Any}. Note that intersection types can be used to specify a disjunction of lower bounds, and a conjunction of upper bounds. Since we mostly use upper bounds, we abbreviate \kind{*(Nothing, T)} to \kind{*(T)}, and \kind{*(Nothing, Any)} is written as \kind{*}.


\begin{figure}
  \centering
\begin{verbatim}
  Kind ::= `*(' Type `,' Type `)' 
         | [id `@' ] Kind `->' Kind
\end{verbatim}
  \caption{Kinds (not in surface syntax)}
  \label{lst:scala:syntax:kinds}
\end{figure}

% TODO: elaborate, make clearer that this refers to second line of syntax definition
We refine the kind of type constructors by turning it into a \emph{dependent} function kind, as higher-order type parameters may appear in their own bounds, or in the bounds of their outer type parameter.  

In the examples that was introduced above, \type{Container[X]} introduces a type constructor parameter of kind \kind{* -> *}, and \type{Container[X] <: Iterable[X]} implies the kind \kind{X @ * -> *(Iterable[X])} for \type{Container}. Finally, the declaration  \type{C[X <: Ordered[X]] <: Iterable[X]} results in \type{C} receiving the kind \kind{X @ *(Ordered[X]) -> *(Iterable[X])}. Again, the syntax for higher-order type parameters provides all the necessary information to infer a (dependent) function kind for type constructor declarations.




Informally, type constructor polymorphism introduces an indirection through the kinding rules in the typing rule for type application, so that it uniformly applies to generic classes, type constructor parameters, and abstract type constructor members. These type constructors, whether concrete or abstract, are assigned function kinds by the kind system. Thus, if \type{T} has kind \kind{X @ K -> K'}, and \type{U} has kind \type{K}, in which \type{X} has been replaced by \type{U}, a type application \type{T[U]} has kind \type{K'}, with the same substitution applied. Multiple type arguments are supported through the obvious generalisation (taking the necessary care to perform simultaneous substitutions).

\subsection{Subkinding}
Similar to the subtyping relation that is defined on types, subkinding relates kinds. Thus, we overload \code{<:} to operate on kinds as well as on types. As the bounds-tracking kind stems from Scala's bounds on type declarations, subkinding for this kind simply follows the rules that were already defined for type member conformance: \kind{*(T, U) <: *(T', U')} if \type{T' <: T} and \type{U <: U'}. Intuitively, this amounts to interval inclusion. For the dependent function kind, we transpose subtyping of dependent function types \cite{DBLP:journals/tcs/AspinallC01} to the kind level.


\subsection{Example: why kinds track bounds \label{sec:example:kinds:track:bounds}}
Suppose \type{Iterable}\footnote{For simplicity, we define \type{Iterable} using type parameters in this example.} is subclassed as in Listing \ref{lst:numlistmem}. This program is rejected by the compiler because the type application \type{Iterable[NumericList, T]} is ill-kinded. The kinding rules classify \type{NumericList} as a \kind{*(Number) -> *}, which must be a subkind of the expected kind of \type{Iterable}'s first type parameter, \kind{* -> *}. Now, \kind{*(Number) <: *}, whereas subkinding for function kinds requires the argument kinds to vary contravariantly. 

Intuitively, this type application must be ruled out, because passing \type{NumericList} as the first type argument to \type{Iterable} would ``forget'' that \type{NumericList} may only contain \type{Number}'s: \type{Iterable} is kind-checked under the assumption that its first type argument does not impose any bounds on its higher-order type parameter, and it could thus apply \type{NumericList} to, say, \type{String}. The next section elaborates on this.
 
\begin{lstlisting}[float,label=lst:numlistmem,caption=\type{NumericList}: an illegal subclass of \type{Iterable}]
class Iterable[Container[X], T]
trait NumericList[T <: Number] extends Iterable[NumericList, T]
\end{lstlisting}

Fortunately, \type{Iterable} can be defined so that it can accommodate bounded collections, as shown in Listing \ref{lst:numlistbound}. To achieve this, \type{Iterable} abstracts over the bound on \type{Container}'s type parameter. \type{NumericList} instantiates this bound to \type{Number}. We refine this example in Section \ref{sec:boundediter}.


\begin{lstlisting}[float,label=lst:numlistbound,caption=Safely subclassing \type{Iterable}]
class Iterable[Container[X <: Bound], T <: Bound, Bound]

trait NumericList[T <: Number] extends Iterable[NumericList, T, Number]
\end{lstlisting}


\subsection{Kind soundness \label{sec:embedding:kindsoundness}}
Analogous to type soundness, which provides guarantees about value-level abstractions, kind soundness ensures that type-level abstractions do not go ``wrong''. 

At the value level, passing, e.g., a \type{String} to a function that expects an \type{Integer} \emph{goes wrong} when that function invokes an \type{Integer}-specific operation on that \type{String}. Type soundness ensures that application is type-preserving, in the sense that a well-typed application evaluates to a well-typed result.

As a type-level example, consider what happens when a type function that expects a type of kind \kind{* -> *}, is applied to a type of kind \kind{*(Number) -> *}. This application \emph{goes wrong}, even though the type function itself is well-kinded, if it does something with that type constructor that would be admissible with a type of kind \kind{* -> *}, but not with a type of kind \kind{*(Number) -> *}, such as applying it to \type{String}. If the first, erroneous, type application were considered well-kinded, type application would not be kind-preserving, as it would turn a well-kinded type into a nonsensical, ill-kinded, one (such as \type{NumericList[String]}).

As our kind system is closely related to dependently typed lambda calculus with subtyping, it is reasonable to assume that it is sound. Proving this conjecture, as well as the more familiar meta-theoretic results, is ongoing work. The underlying theory -- an object-oriented calculus -- has been described in earlier work \cite{moors08:scalina}. 

Finally, it is important to note that kind unsoundness results in type applications ``going wrong'' \emph{at compile time}. Thus, the problem is less severe than with type unsoundness, but these errors can be detected earlier in the development process, without effort from the programmer.